\begin{tabbing}
FIFO
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$C$:Type\+
\\[0ex]$\times$ ($T$:Type
\\[0ex]$\times$ $S$:($C$$\rightarrow$$C$$\rightarrow$E$\rightarrow\mathbb{P}$)
\\[0ex]$\times$ $R$:($C$$\rightarrow$E$\rightarrow\mathbb{P}$)
\\[0ex]$\times$ ${\it codes}$:($j$,$i$:$C$$\rightarrow$$e$:\{$x$:E$\mid$ $S$($j$,$i$,$x$)\} $\rightarrow$state@loc($e$)$\rightarrow$$T$)
\\[0ex]$\times$ (${\it decodes}$:($i$:$C$$\rightarrow$$e$:\{$x$:E$\mid$ $R$($i$,$x$)\} $\rightarrow$state@loc($e$)$\rightarrow$$T$)
\\[0ex]$\times$ for\= clients $C$ sends FIFO\+
\\[0ex]from j to i via ($S$[j,i],${\it codes}$)
\\[0ex]receives at i via ($R$[i],${\it decodes}$)))
\-\-
\end{tabbing}